package ui;

import java.awt.Toolkit;
import java.awt.datatransfer.StringSelection;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.OutputStream;
import java.io.OutputStreamWriter;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.io.Writer;
import java.util.Vector;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import javax.swing.JFrame;
import javax.swing.JOptionPane;
import javax.xml.transform.stream.StreamSource;
import net.sf.saxon.s9api.Processor;
import net.sf.saxon.s9api.SaxonApiException;
import net.sf.saxon.s9api.Serializer;
import net.sf.saxon.s9api.XdmNode;
import net.sf.saxon.s9api.XsltCompiler;
import net.sf.saxon.s9api.XsltExecutable;
import net.sf.saxon.s9api.XsltTransformer;
import automatica.autoprove.CallBacks;
import com.maplesoft.externalcall.MapleException;
import com.maplesoft.openmaple.Engine;
import static constants.GTextbookConstants.*;

public class Utility{
 
	public static String toPattern(String str){
		StringBuffer result = new StringBuffer();
		if(str!=null){
		char[] chars = new char[str.length()];
		str.getChars(0, str.length(), chars, 0);
		for(int i =0; i<chars.length;i++){
			if(chars[i]=='('|chars[i]==')'|chars[i]=='['|chars[i]==']'|chars[i]=='{'|chars[i]=='}'){
				result.append('\\');	
			}
			result.append(chars[i]);
		}
		}
		return result.toString();
	}
	
	//old version of suqote2dquote
	/*
	public static String squote2dquote(String str){
		StringBuffer result = new StringBuffer();
		if(str!=null){
		char[] chars = new char[str.length()];
		str.getChars(0, str.length(), chars, 0);
		boolean left = false;
		boolean right = false;
		for(int i =0; i<chars.length;i++){
			if(chars[i]=='<'){
				left = true;
				right = false;
			}
			if(chars[i]=='>'){
				right = true;
				left = false;
			}
			if(left==right){
				if(chars[i]== '\''){
					result.append('\'');
					result.append('\'');
				}else
					result.append(chars[i]);
			}else{
				if(chars[i]== '\''){
					result.append('\"');
				}else
					result.append(chars[i]);	
			}
			
		}
		}
		return result.toString();
	}
	*/
	public static String squote2dquote(String str){
		StringBuffer result = new StringBuffer();
		if(str!=null){
			char[] chars = new char[str.length()];
			str.getChars(0, str.length(), chars, 0);
			for(int i =0; i<chars.length;i++){
				if(chars[i]== '\''){
					if(i+1<chars.length&&chars[i+1]!= '\''){
						result.append('\'');
						result.append('\'');
					}
				}else
					result.append(chars[i]);
			}
		}
		return result.toString();
	}

	
	public static Vector<String> getItemsBySemicolon(String str){
		Vector<String> result = new Vector<String>(1,1);
		String reg = ";|；";                        
	    Pattern pattern = Pattern.compile(reg);
	    Matcher m = pattern.matcher(str);
	    int start = 0;
	    int end = str.length();
	    while(m.find()){
	    	result.add(str.substring(start,m.start()));
	    	start=m.end();
	    }
	    if(start!=end){
	    	result.add(str.substring(start,end));
	    }
		return result;
	}
	
	public static Vector<String> getItemsBySeparator(String str, String s){
		Vector<String> result = new Vector<String>(1,1);
		String reg = ";|；|\\"+s;                        
	    Pattern pattern = Pattern.compile(reg);
	    Matcher m = pattern.matcher(str);
	    int start = 0;
	    int end = str.length();
	    while(m.find()){
	    	result.add(str.substring(start,m.start()));
	    	start=m.end();
	    }
	    if(start!=end){
	    	result.add(str.substring(start,end));
	    }
		return result;
	}

//É¾³ýÐÎÊ½Óï¾äÖÐµÄÒªÉ¾³ýµÄÖ¸¶¨×Ö·û£¬\\s£¬;µÈ
  public static String deleteSpace(String test){
      StringBuffer result = new StringBuffer();
      String reg = "\\s";                        //Ö¸¶¨ÒªÉ¾³ýµÄ×Ö·û
      Pattern pattern = Pattern.compile(reg);
      Matcher m = pattern.matcher(test);      
      Vector<Integer> spaceIndex = new Vector<Integer>(10,10);
      int start = 0;
      int end = 0;
      while( m.find() ){
      spaceIndex.add(m.start());                   //±ê¼ÇÒªÉ¾³ýµÄ×Ö·û
     }
     if(spaceIndex.isEmpty())
      return test;
     else{
         for(int i = 0; i < spaceIndex.size();i++){          
            end = spaceIndex.get(i);
            if(start == end){
               start = end+1;
            if(start > test.length()-1)
              break;
            if(i == spaceIndex.size()-1)
               end = test.length();
            else{                 
               end = spaceIndex.get(i+1);
               continue;
            }
            }  
            result.append(test.substring(start,end));
            start = end +1;
            if(start > test.length())
               break;        
         }
         if(start <= test.length()-1){      
         end = test.length();
         result.append(test.substring(start,end));
         }
     return result.toString();
        }
    }
     
      

   
   //Éú³É×Ó¾äÄ£Ïî,µÚÒ»Î»ÎªÎ½´Ê£¬ÒÔºó¸÷Î»ÎªÏî
   public static Vector<String> generateTermSet(String test){
      int[][] t = matchPairs(test);
    //  System.out.println("The pairs of parentheses are: ");
      //for(int i = 0; i < t.length; i++){
     //    System.out.println("start " + t[i][0] + " end "+ t[i][1]);
      //}
      Vector<String> term = new Vector<String>(5,5);
      term.add(test.substring(0,t[0][0]));
      int begin = t[0][0]+1;
      int over = 0;
      while(begin < test.length()){
         for(int point = begin;point < test.length();point++){
            if(test.charAt(point)=='('||test.charAt(point)=='（'){
               for(int y = 0;y < t.length;y++){
                  if(t[y][0] == point)
                    { 
                    point = t[y][1]+1;
                  //  System.out.println("The mark of extracted term: "+ t[y][1]);
                    break;
                    }
                                          
               }
            }
            if(test.charAt(point)==','||test.charAt(point)=='；'||test.charAt(point)==')'||test.charAt(point)=='）'){
               over = point;
               break;
            }
            
         }  
            
         //È·¶¨ÖÕµã
         if(begin!=over){
         term.add(test.substring(begin,over));
         System.out.println("Start: " + begin + "||Over: " + over);
         }									//ÌáÈ¡Ïî
         begin = over+1;                                //ÖØÐÂÌáÈ¡ 


        
       
         
      }
    //  System.out.println("The size of termSet: " + term.size());
     // System.out.println("The term in termSet are:\n");
     // for(int index = 0; index < term.size();index++){        
      //  System.out.println(index + " " + term.get(index));
      //}
      return term;
   }
   
   //À¨ºÅÅä¶Ô
  public static int[][] matchPairs(String test){
      
      Vector<Integer> textBone = new Vector<Integer>(10,10);
      String regEx = "\\(|\\)|\\（|\\）";
      Pattern pattern = Pattern.compile(regEx);
      Matcher m = pattern.matcher(test);
      
     while( m.find() ){
   //   System.out.println("Parentheses found at Start: "+m.start());
      textBone.add(m.start());
     }
     
     int[][] pairs = new int[textBone.size()/2][2];
     int count = 0;
     int start = 0;
     int end = 0;
     int n = 0;
    
    for(int j = 0; j < textBone.size(); j++){
      start = textBone.get(j);
      if (textBone.get(j)==0)
         continue;
      else{      
         int t = j;
         do {
            if (test.charAt(textBone.get(t))=='('||test.charAt(textBone.get(t))=='（'){
               count++;
               t++;
            }
            if (test.charAt(textBone.get(t))==')'||test.charAt(textBone.get(t))=='）'){
               count--;
               t++;
            }   
         }while(count!=0);
         end = textBone.get(t-1);
         textBone.set(t-1,0);
         t++;
         pairs[n][0] = start;  //½«Åä¶ÔµÄ½á¹ûÐ´Èë¶þÎ»Êý×é
         pairs[n][1] = end;
         n++;
      }
   }
  return pairs;
}
  
  public static Vector<String> generateTermSetWithSpace(String test, char left, char right){
	 //test = deleteSpace(test);
	  test = test.trim();
     int[][] t = matchPairs(test,left,right);
   //  System.out.println("The pairs of parentheses are: ");
     //for(int i = 0; i < t.length; i++){
    //    System.out.println("start " + t[i][0] + " end "+ t[i][1]);
     //}
     Vector<String> term = new Vector<String>(5,5);
     term.add(test.substring(0,t[0][0]));
     int begin = t[0][0]+1;
     int over = 0;
     while(begin < test.length()){
        for(int point = begin;point < test.length();point++){
           if(test.charAt(point)==left||test.charAt(point)=='('){
              for(int y = 0;y < t.length;y++){
                 if(t[y][0] == point)
                   { 
                   point = t[y][1]+1;
                 //  System.out.println("The mark of extracted term: "+ t[y][1]);
                   break;
                   }
                                         
              }
           }
           if(test.charAt(point)==','||test.charAt(point)==right||test.indexOf(point)=='；'||test.charAt(point)==')'){
              over = point;
              break;
           }
           
        }  				//È·¶¨ÖÕµã
        
        if(begin!=over || begin > over){
       	 term.add(test.substring(begin,over));       //ÌáÈ¡Ïî
        }
        begin = over+1;                                //ÖØÐÂÌáÈ¡ 
        
     }
   //  System.out.println("The size of termSet: " + term.size());
    // System.out.println("The term in termSet are:\n");
    // for(int index = 0; index < term.size();index++){        
     //  System.out.println(index + " " + term.get(index));
     //}
     return term;
  }
  
  
 
 public static int[][] matchPairs(String test, char left, char right){
     Vector<Integer> textBone = new Vector<Integer>(10,10);
     String regEx = "\\" +left+"|"+ "\\"+right+"|\\(|\\)";
     Pattern pattern = Pattern.compile(regEx);
     Matcher m = pattern.matcher(test);
     
    while( m.find() ){
  //   System.out.println("Parentheses found at Start: "+m.start());
     textBone.add(m.start());
    }
    
    int[][] pairs = new int[textBone.size()/2][2];
    int count = 0;
    int start = 0;
    int end = 0;
    int n = 0;
   
   for(int j = 0; j < textBone.size(); j++){
     start = textBone.get(j);
     if (textBone.get(j)==0)
        continue;
     else{      
        int t = j;
        do {
           if (test.charAt(textBone.get(t))==left||test.charAt(textBone.get(t))=='('){
              count++;
              t++;
           }
           if (test.charAt(textBone.get(t))==right||test.charAt(textBone.get(t))==')'){
              count--;
              t++;
           }   
        }while(count!=0);
        end = textBone.get(t-1);
        textBone.set(t-1,0);
        t++;
        pairs[n][0] = start;  //½«Åä¶ÔµÄ½á¹ûÐ´Èë¶þÎ»Êý×é
        pairs[n][1] = end;
        n++;
     }
  }
 return pairs;
}
  
   //¼ì²âÓÐÎÞÎ½´Ê
   public static boolean havePredicate(String test){
      String reg = "\\(|\\（";
      Pattern pattern = Pattern.compile(reg);
      Matcher m = pattern.matcher(test);
      if(m.find())
      return true;
      else
      return false;
   }
   
   
   
   
      
      
     public static Vector<String> generateOM(String name, String reference, String...args){
      
      Vector<String> patOM = new Vector<String>(5,5);
      
      patOM.add("<OMA><OMS cd=\""+ reference + "\" name=\"" + name + "\"/>\n");
      
      for(int i=0; i< args.length; i++){
      	patOM.add(args[i]);
      }
      
      patOM.add("</OMA>\n");
      
      return patOM;
      
      }
      
    
      
      
      public static Vector<String> extractPoint(String str){
      	Vector<String> term = new Vector<String>(5,5);
      	Vector<String> buf = new Vector<String>(5,5);
      	term = generateTermSet(str);
      	if(!term.get(0).equals("integer"))
      		
      		for(int i = 1; i < term.size(); i++){
      		
      		   if(havePredicate(term.get(i)))
      		      buf.addAll(extractPoint(term.get(i)));
      		   else
      		      buf.add(term.get(i));
      	     }
      	
      	return buf;
      }
      
      public static Vector<String> reduce(Vector<String> pointList){
      	if(pointList.size()==1)  return pointList;
      	else{     	
      	  for(int i = 0; i < pointList.size()-1; i++){
      		for(int j = i + 1; j < pointList.size(); j++){
      			if(pointList.get(i).equals(pointList.get(j))){
      				pointList.remove(j);
      				reduce(pointList);
      			}
      		 }
      	  }
      	}
      	
      	return pointList;
      }
      
      
  public static String putIndent(int blank){
      StringBuffer buf = new StringBuffer(10);
      for(int i = 0; i < blank; i++){
            	buf.append(Indent);
            }
      return buf.toString();
      }
  
  //connect to SQL server 2000
  /*
  public static Connection createConnection(String dataBaseName, String user, String password){
	  Connection con = null;
	  String url = constants.GTextbookConstants.DriverURL+dataBaseName;
	  
	  try{    
          
		  Class.forName(constants.GTextbookConstants.DriverName);

          con = DriverManager.getConnection( url, user, password );

      }
      catch(Exception err){
    	  LangWarningPane.showMessageDialog(null,"Cannot connect to the DATABASE!", "连接数据库错误!", "Connection Error", "连接错误", JOptionPane.ERROR_MESSAGE, language.getNum());			
          err.printStackTrace(System.out);
      }
      
      return con;

  }
  */
  
  /*
  public static Connection createConnection(String dataBaseName, String user, String password){
	  Connection con = null;
	  String url = "jdbc:mysql://localhost/"+dataBaseName;
      try{    //ÕâÀïµÄÒì³£´¦ÀíÓï¾äÊÇ±ØÐèµÄ.·ñÔò²»ÄÜÍ¨¹ý±àÒë! 
          Class.forName("com.mysql.jdbc.Driver");
          //System.out.println("driver successful!");

          con = DriverManager.getConnection( url,user, password );
         
          if(!con.isClosed()){
        	  //System.out.println("Succeed connecting to the database!");
          }
          
      }
      catch(Exception err){
          err.printStackTrace(System.out);
      }
      
      return con;

  }
  */
  
  //decide whether A exist in list B
  public static boolean existIn(String A, Vector<String> B){
	  boolean result = false;
	  for(int i = 0; i < B.size(); i++){
		  if(A.equals(B.elementAt(i))){
			  result = true;
			  break;
		  }
	  }
	  
	  
	  return result;
  }
  
  
  /*
   * transform the file of sourcePath into a file of resultPath using xsl of xslPath
   */
  public static void transformation(String sourcePath, String xslPath, String resultPath, String type)throws SaxonApiException{
		
		Processor proc = new Processor(false);
      XsltCompiler comp = proc.newXsltCompiler();
      XsltExecutable exp = comp.compile(new StreamSource(new File(xslPath)));
      XdmNode source = proc.newDocumentBuilder().build(new StreamSource(new File(sourcePath)));
      Serializer out = new Serializer();
      out.setOutputProperty(Serializer.Property.METHOD, type);
      out.setOutputProperty(Serializer.Property.INDENT, "no");
      out.setOutputFile(new File(resultPath));
      XsltTransformer trans = exp.load();
      trans.setInitialContextNode(source);
      trans.setDestination(out);
      trans.transform();
	}
	

	  
	  public static void saveFile(JFrame window, String content, File outFile) {
		     
		    FileOutputStream outputFile = null;     // Place to store the stream reference
		    try {
		    	
		    	if(content != null){
		    		outputFile = new FileOutputStream(outFile, false);
		                                
		    		System.out.println("File stream created successfully.");
		    		
		    		
		    		
		    		// important
		    		Writer w = new OutputStreamWriter(outputFile, "UTF-8"); 
      
		    		w.write(content);
		    		w.close();
		    		System.out.println("File contents written to file.");
		    	}else{
		    		System.out.println("The content is null");
		    	}
		      
		    } catch (FileNotFoundException e) {
		      e.printStackTrace(System.err);
		    } catch(IOException e) {
		      System.err.println(e);
		      JOptionPane.showMessageDialog(window,
		                                    "Error writing a file.",
		                                    "File Output Error",
		                                    JOptionPane.ERROR_MESSAGE);
		      return;                                    // Serious error - return
		    }
		           
	}
	  
	  public static String readFile(String path) throws IOException{
          InputStream  is  =  new  FileInputStream(path);
          StringBuffer  buffer  =  new  StringBuffer();
          readToBuffer(buffer,  is);
          //System.out.println(buffer);          //  ½«¶Áµ½  buffer  ÖÐµÄÄÚÈÝÐ´³öÀ´
          is.close();
          return buffer.toString();
	  }
	  
      public  static void  readToBuffer(StringBuffer  buffer,  InputStream  is)throws  IOException  {
    	  String  line;                //  ÓÃÀ´±£´æÃ¿ÐÐ¶ÁÈ¡µÄÄÚÈÝ
    	  BufferedReader  reader  =  new  BufferedReader(new  InputStreamReader(is));
    	  line  =  reader.readLine();              //  ¶ÁÈ¡µÚÒ»ÐÐ
    	  while  (line  !=  null)  {                    //  Èç¹û  line  Îª¿ÕËµÃ÷¶ÁÍêÁË
              buffer.append(line);                //  ½«¶Áµ½µÄÄÚÈÝÌí¼Óµ½  buffer  ÖÐ
              buffer.append("\n");                //  Ìí¼Ó»»ÐÐ·û
              line  =  reader.readLine();      //  ¶ÁÈ¡ÏÂÒ»ÐÐ
    	  }
      }
      
      /**
       *  2.  ÑÝÊ¾½«  StringBuffer  ÖÐµÄÄÚÈÝ¶Á³öµ½Á÷ÖÐ
       */
     public  void  writeFromBuffer(StringBuffer  buffer,  OutputStream  os)  {
             //  ÓÃ  PrintStream  ¿ÉÒÔ·½±ãµÄ°ÑÄÚÈÝÊä³öµ½Êä³öÁ÷ÖÐ
             //  Æä¶ÔÏóµÄÓÃ·¨ºÍ  System.out  Ò»Ñù
             //  £¨System.out  ±¾Éí¾ÍÊÇ  PrintStream  ¶ÔÏó£©
             PrintStream  ps  =  new  PrintStream(os);      
             ps.print(buffer.toString());
     }
     /**
       *  3*.  ´ÓÊäÈëÁ÷ÖÐ¿½±´ÄÚÈÝµ½ÊäÈëÁ÷ÖÐ
       *  @throws  IOException
       */
     public  void  copyStream(InputStream  is,  OutputStream  os)  throws  IOException  {
             //  Õâ¸ö¶Á¹ý¹ý³Ì¿ÉÒÔ²ÎÔÄ  readToBuffer  ÖÐµÄ×¢ÊÍ
             String  line;
             BufferedReader  reader  =  new  BufferedReader(new  InputStreamReader(is));
             PrintWriter  writer  =  new  PrintWriter(new  OutputStreamWriter(os));
             line  =  reader.readLine();
             while  (line  !=  null)  {
                     writer.println(line);
                     line  =  reader.readLine();
             }
             writer.flush();          //  ×îºóÈ·¶¨Òª°ÑÊä³öÁ÷ÖÐµÄ¶«Î÷¶¼Ð´³öÈ¥ÁË
                                                     //  ÕâÀï²»¹Ø±Õ  writer  ÊÇÒòÎª  os  ÊÇ´ÓÍâÃæ´«½øÀ´µÄ
                                                     //  ¼ÈÈ»²»ÊÇ´ÓÕâÀï´ò¿ªµÄ£¬Ò²¾Í²»´ÓÕâÀï¹Ø±Õ
                                                     //  Èç¹û¹Ø±ÕµÄ  writer£¬·â×°ÔÚÀïÃæµÄ  os  Ò²¾Í±»¹ØÁË
     }
	
			
			public static void executeBatFile(String path, String filename){
				String command = "cmd /C start /D \""+path+"\" /min " + filename;
				
				try {    
			        Process child = Runtime.getRuntime().exec(command);    
			        InputStream in = child.getInputStream();    
			        int c;    
			        while ((c = in.read()) != -1) {    
			            System.out.print(c);    
			        }    
			        in.close();    
			        try {    
			            child.waitFor();    
			        } catch (InterruptedException e) {    
			            // TODO Auto-generated catch block    
			            e.printStackTrace();    
			        }    
			        //System.out.println("done");    
			    } catch (IOException e) {    
			        // TODO Auto-generated catch block    
			        e.printStackTrace();    
			    }
			}

			public static Engine buildEngine4Maple(CallBacks callback){
				
				 Engine engine;
				 
				  /* build the command line arguments for Maple */
					String a[];
			        a = new String[1];
			        a[0] = "java";
			        
			        try
			        {
			            /* start the Maple session.  Use the Default EngineCallBacks. 
			             * the text Output will be directed to System.out */
			            engine = new Engine(a,callback,null, null );
			            engine.evaluate( "with(geother);");
			            return engine;
			        }
			        catch ( MapleException e1 )
			        {
			            /* if an error occurs, exit */
			        	LangWarningPane.showMessageDialog(null,"Cannot connect to Maple！Cannot use GEOTHER！", "无法连接到Maple！无法使用GEOTHER！", "Auto Proving Disabled", "自动证明不可用", JOptionPane.ERROR_MESSAGE, language.getNum());			
			        	System.out.println(e1);
			            System.out.println( "An exception occured\n" );
			            return null;
			        }  
			}
			
			
			public static String getFormalString4Script(String data, String ndg){
				StringBuffer result = new StringBuffer(10);
				result.append("Script(");
				
				int index = data.indexOf("\u225D");
				
				String instance = data.substring(0,index);
				String body = data.substring(index+1,data.length());
				
				result.append("Definition(" + instance +","+body+","+ndg+")");
				
				
				result.append(")");			
				return result.toString();
			}
			
			
			public static String getFormalString4Multiple(String data,String name, String role){
				StringBuffer result = new StringBuffer(10);
				result.append("Problems(");
				int index = data.indexOf("<=>");
				if(index !=-1 ){
					String hypothesisString = data.substring(0,index);
					String conclusionString = data.substring(index+3,data.length());
					
					result.append(getFormalString4Single(hypothesisString + "=>" +conclusionString, name+"_forward", role));
						
					
					
					Vector<String> H = Utility.getItemsBySemicolon(hypothesisString);
					String newConclusion = H.get(H.size()-1);
					StringBuffer buf = new StringBuffer(20);
					for(int i = 0; i < H.size()-1; i++){
						buf.append(H.get(i)+";");
					}
					buf.append(conclusionString+"=>"+newConclusion);
					
					result.append(","+getFormalString4Single(buf.toString(),name+"_backward",role)+")");
					
				}else{
					index = data.indexOf("=>");
					if(index!=-1){
						result.append(getFormalString4Single(data,name,role)+")");
					}
				}
				
				return result.toString();
			}
			
			
			
			public static String getFormalString4Single(String data, String name, String role){
				StringBuffer result = new StringBuffer(10);
				int index = data.indexOf("=>");
				if(index !=-1){
					String hypothesisString = data.substring(0,index);
					String conclusionString = data.substring(index+2,data.length());
					StringBuffer buf = new StringBuffer(100);
					if(hypothesisString.indexOf("configuration")!=-1){
						buf.append(hypothesisString.replace("configuration", "assume"));
					}else{
						Vector<String> H = Utility.getItemsBySemicolon(hypothesisString);
						buf.append("assume(");
						for(int i = 0; i < H.size()-1; i++){
							buf.append(H.get(i)+",");
						}
						buf.append(H.get(H.size()-1)+")");
					}
					StringBuffer buf1 = new StringBuffer(100);
					if(conclusionString.indexOf("configuration")!=-1){
						buf1.append(conclusionString.replace("configuration", "show"));
					}else{
						Vector<String> C = Utility.getItemsBySemicolon(conclusionString);
						buf1.append("show(");
						for(int i = 0; i < C.size()-1; i++){
							buf1.append(C.get(i)+",");
						}
						buf1.append(C.get(C.size()-1)+")");
					}
					
					result.append("Theorem(" + name + "," + role + "," + buf.toString() + "," + buf1.toString() +")");
					
				}
				return result.toString();
			}
			
			
			public static String getEnglishRole(String role){
				String result = role;
					if(role.equals("定义")){
						result = "Definition";
					}
					else if(role.equals("引理")){
						result = "Lemma";
					}
					else if(role.equals("定理")){
						result = "Theorem";
					}
					else if(role.equals("推论")){
						result = "Corollary";
					}
					else if(role.equals("公理")){
						result = "Axiom";
					}else if(role.equals("猜想")){
						result = "Conjecture";
		
					}
					else if(role.equals("问题")){
						result = "Problem";

					}
					else if(role.equals("例子")||role.equals("例")){
						result = "Example";
						
					}
					else if(role.equals("练习")){
						result = "Exercise";
					
					}
					else if(role.equals("证明")){
						result = "Proof";
						
					}
					else if(role.equals("解答")||role.equals("解")){
						result = "Solution";
						
					}
					else if(role.equals("介绍")||role.equals("引言")){
						result = "Introduction";
						
					}
					else if(role.equals("注释")||role.equals("注")){
						result = "Remark";
						
					}
					else if(role.equals("算法")){
						result = "Algorithm";
						
					}else if(role.equals("类型")){
						result = "Type";				
					}
					return result;
			}
			
		public static void copy(String str){
			StringSelection st = new StringSelection(str);
			Toolkit.getDefaultToolkit().getSystemClipboard().setContents(st, st);
		}
			

}


